| Definitions | t  T, IdDeq,  x:A. B(x), Id,  b, Action(i), x:A  B(x), P   Q, IdLnk, #$n, A B, a<b, Void, False,  A,  , {x:A| B(x) },  , A & B, x:A B(x), P & Q, {T}, f(x), x dom(f), mk-ma, x : v, f(x)?z, z != f(x) P(a;z), only members of L affect x :t, M.ds(x), M.bframe(k sends on l), M(i), @i: only L affects x : t, M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), M.pre(a,s,v), M.init(x,v), PossibleWorld(D;w), E, es_val(es), es-Trans(es), es_init(es), es-pred?(es), es_info(es), (state when e), state after e, es-T(es), x when e, ES(the_w), (x after e), kind(e), loc(e), E, vartype(i;x), s = t, Knd, (x l), FairFifo, World, D realizes2 es.P(es), e@i. P(e), @i only events in L change x : T, es is an event system of D, ES, Type, Prop,  x.A(x),  x. t(x), type List, D realizes es. P(es), act(e), kind(e), SQType(T), True, kind(a), s(i;t).x, <a,b>, (x when e), (x after e), n+m, KindDeq, deq-member(eq;x;L), P  Q, P Q, f(a), Atom$n, loc(e), time(e), w-info(w;e), loc(e), kind(e), s ~ t, vartype(i;x), a(i;t), isnull(a), state_after(e), s.x, state_when(e) |